Nuprl Lemma : inl_wf
11,40
postcript
pdf
x
:Top. (inl
x
)
Decision
latex
Definitions
Decision
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
top
wf
origin
x:Top. (inl x ) 
Decision x:Top. (inl x ) Decision Tx:A. B(x)